%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Author: Jose Santos <jcas81@gmail.com>
% Date: 2009-09-08
%
%    This file contains predicates to perfectly reduce a clause using its full failing profile
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

/*

Notes: the idea of computing a perfect_armg, although appealing, does not work because the literals
are not independent. That is: when we remove a literal that potentially affects the failing profile
of all the other examples. Eg. If we remove literal [2] we could think that has nothing to do with
a clause that has failing profile, say, [5,17,28], however, with the 2 removed, the failing profile
for the last example could be very different! (or none at all)

% this applies for problem m16l12
:- ['source/bottom clause/perfect_armg'].

testPerfectARMG(Example):-
  sat(Example, Clause, ClauseSig),
  examples:exampleIDs(PosEIDs, NegEIDs),
  perfect_armg(Clause, ClauseSig, PosEIDs, NegEIDs, PA, _PAS, _PosCov, _NegCov),
  portray_clause(PA),nl.

%testClauseCoverage(Example, IndexsToRemove):-
testClauseCoverage(Iteration):-
  Example=p(d1),
  iter(Iteration, IndexsToRemove),
  sat(Example, Clause, ClauseSig),
  examples:exampleIDs(PosEIDs, NegEIDs),
  perfect_armg:remove_indexs_from_clause(Clause, ClauseSig, IndexsToRemove, NClause, NClauseSig),
  coverage:full_hypothesis_coverage(NClause, NClauseSig, PosEIDs, NegEIDs, PosEIDsCov, NegEIDsCov),
  length(PosEIDsCov, NumPos),
  length(NegEIDsCov, NumNegs),
  format("Test clause coverage. NumPos:~w NumNeg:~w~n", [NumPos, NumNegs]),
  format("PosEIDsCov:~w~nNegEIDsCov:~w~n", [PosEIDsCov, NegEIDsCov]).


iter(1,[33,38,39,41,42,43,45,47,49,50,53,55,58,66,68,72,76,77,79,81,84,92,93]).
iter(2,[28,31,33,35,38,39,41,42,43,44,45,46,47,48,49,50,53,55,56,58,63,66,67,68,70,72,75,76,77,78,79,81,82,83,84,88,90,92,93]).
iter(3,[28,31,33,35,36,38,39,40,41,42,43,44,45,46,47,48,49,50,53,55,56,57,58,62,63,64,66,67,68,70,72,73,75,76,77,78,79,81,82,83,84,88,90,91,92,93]).
iter(4,[28,31,33,35,36,38,39,40,41,42,43,44,45,46,47,48,49,50,53,55,56,57,58,62,63,64,65,66,67,68,69,70,72,73,75,76,77,78,79,80,81,82,83,84,88,90,91,92,93]).
iter(5,[28,31,33,35,36,38,39,40,41,42,43,44,45,46,47,48,49,50,51,53,55,56,57,58,62,63,64,65,66,67,68,69,70,72,73,75,76,77,78,79,80,81,82,83,84,88,90,91,92,93]).
iter(6,[28,30,31,33,35,36,38,39,40,41,42,43,44,45,46,47,48,49,50,51,53,55,56,57,58,62,63,64,65,66,67,68,69,70,72,73,75,76,77,78,79,80,81,82,83,84,87,88,90,91,92,93]).
*/
:- module(perfect_armg,
          [
            perfect_armg/8
          ]
         ).

% GILPS modules
:- use_module('../settings/settings', [setting/2]).
:- use_module('../examples/examples', [id2example/2, exampleIDsWeights/2]).
:- use_module('../hypotheses/score', [hypothesis_info/5, score/3, verifies_partial_metrics/2]).
:- use_module('../messages/messages', [message/2]).
:- use_module('clause_reduce', [examplesFullFailingProfile/4, negative_clause_reduce/10]).

% YAP modules
:- use_module(library(lists), [reverse/2]).
:- use_module(library(ordsets), [ord_union/3, ord_subset/2, ord_subtract/3, ord_insert/3]).


posFP([1-[32,65,71,73,81,82,85,89,93],2-[],3-[32,33,37,38,40,41,42,50,53,58,65,69,71,83,84,92],4-[33,37,41,55,61,71,75,84,89,90,91,93],5-[31,36,40,42,51,53,57,58,68,75,77,79,82,83,93],6-[31,33,47,48,63,79,85,89,93],7-[38,49,57,62,63,65,70,76,87,88,91],8-[39,42,45,53,59,61,64,67,71,72,73,81,84,85,91,93],9-[32,33,35,48,49,50,63,67,87],10-[30,33,35,38,40,53,57,58,59,60,61,62,63,65,66,69,72,93],11-[37,39,47,49,51,61,64,68,70],12-[31,32,45,47,49,58,61,66,68,80,81,85,90,91],13-[31,32,42,48,52,59,61,64,66,73,81,88,89,91,93],14-[38,57,58,62,69,70,72,91,92],15-[38,46,51,60,62,64,71,77,79,80,81,84,85,91],16-[36,39,53,63,71,73,80,85,88,90],17-[31,36,38,47,48,49,58,59,61,66,69,70,71,85,88],18-[31,37,43,48,53,56,58,60,61,65,75,76,80,90,93],19-[36,45,59,61,71,83],20-[27,29,40,45,46,48,52,59,67,70,73,82,83,89,91,92],21-[29,33,37,43,45,56,59,62,67,71,72,84,91],22-[29,37,38,52,66,75,80,82,85,88,90,92],23-[30,35,36,38,41,45,50,52,56,63,68,70,79,80,84,90,91],24-[28,32,33,43,45,48,61,63,68,69,70,71,75,79,88,90],25-[39,41,42,51,56,59,63,67,70,71,72,76,78,79,83,88,92],26-[36,41,53,62,68,70],27-[33,45,59,61,72,79,81,82,83,91,92,93],28-[38,43,48,56,72,76,77,79,82,90,93],29-[32,37,44,46,48,52,61,62,67,69,70,72,77,81,82,85,88],30-[26,30,33,37,43,46,51,53,55,62,80,81,82,84,85,93],31-[41,43,61,70,76,77,79,91,92],32-[47,51,55,56,57,60,67,69,77,85,88],33-[27,28,30,32,35,36,45,47,51,59,65,67,70,73,74,78],34-[33,38,42,50,59,60,66,67,71,75,80,82,89],35-[40,41,42,44,48,49,58,67,72,73,75,79,82,84,87,88,90],36-[29,38,41,48,49,50,85,88],37-[29,39,50,52,60,64,67,73,75,83,85,89,91,93],38-[38,40,56,61,69,70,73,76,92],39-[38,41,42,47,52,59,60,62,63,65,66,69,71,83,85,92,93],40-[29,31,33,48,49,58,59,62,63,64,67,68,69,70,73,83,84,92],41-[30,33,55,64,68,71,72,73,77,83,90,93],42-[38,43,45,56,57,58,62,72,75,77,80,82,87,88,89,90],43-[43,46,51,55,59,60,61,70,71,73,83,88],44-[33,35,39,42,43,45,49,55,56,60,61,62,63,67,70,71,77,79,88,91],45-[30,32,39,51,57,59,60,65,69,70,75,85],46-[37,38,47,49,52,56,62,63,66,67,74,75,77,79,80,83,85,89],47-[36,40,45,56,67,68,73,75,82,85,88],48-[40,44,63,65,67,77,91,93],49-[33,35,40,42,57,72,73,77,83,90,92],50-[32,36,38,39,43,51,58,65,66,76,79,82,83,85,91],51-[36,39,41,47,49,51,59,61,63,67,79,80,81,84,90,91,93],52-[37,40,50,59,67,69,75,81,84,90,91],53-[32,35,43,55,62,63,64,71],54-[30,32,37,47,51,55,56,59,63,71,75,80,81,82,83,88,91],55-[39,40,41,42,47,50,52,59,72,82,84],56-[37,42,60,62,65,74,75,80,91],57-[38,47,50,51,56,59,61,65,70,77,80,81,82,83,84,85,92],58-[48,50,53,59,62,67,77,79,81,87,92,93],59-[38,39,41,42,45,53,55,70,78,79,80,89,90,91,93],60-[36,39,40,43,45,47,51,53,62,70,72,73,83],61-[33,35,41,45,47,48,61,63,64,70,72,73,80,84,92],62-[28,33,37,39,40,45,47,48,53,56,57,60,62,65,68,69,82,83,90,92],63-[35,43,49,61,64,67,70,73,80,81,84,89,90,91],64-[41,43,45,51,56,60,68,69,71,79,81,88,89,90,91],65-[35,45,51,63,66,71,76,77,91],66-[32,35,37,40,42,46,47,50,51,59,61,69,71,76,83,85,93],67-[37,38,42,45,56,59,60,63,69,84,88],68-[29,37,38,41,43,45,48,58,61,66,67,68,70,77,83,88,92],69-[32,33,36,43,47,49,57,59,62,73,76,78,83,85,91,92],70-[46,48,55,58,65,67,68,70,73,80,82,88,90,92,93],71-[40,42,47,51,52,55,63,69,73,75,82,88,89,92,93],72-[50,56,57,63,65,68,71,72,75,76,77,82,83,91,92],73-[39,40,42,45,47,59,66,68,71,75,82,90,91,92],74-[33,45,47,49,63,69,72,75,77,80,82,85,88,91],75-[38,46,56,57,58,65,67,76,80,82],76-[32,37,41,42,49,56,81,83,89,91],77-[35,36,39,43,48,49,58,59,62,72,84,89,93],78-[35,37,38,40,56,57,63,69,79],79-[36,37,41,57,65,76,80,89,92,93],80-[38,39,41,43,55,61,62,69,78,89,93],81-[30,32,43,50,59,61,63,64,65,73,82,88],82-[39,56,57,59,60,61,65,69,81,82,85],83-[26,31,38,39,42,43,45,48,57,58,63,65,68,83,85,91],84-[28,31,35,38,44,46,48,49,56,58,63,67,70,75,78,79,81,82,83,88,90,93],85-[32,40,43,49,53,58,62,66,68,72,84,85,87],86-[32,39,55,60,61,69,70,75,80,88,93],87-[37,40,41,61,62,63,70,71,77,81,82,89,91,93],88-[32,38,39,42,44,46,48,49,51,55,57,58,59,64,71,74,79,80,82],89-[31,36,43,53,56,60,71,72,83,84,88,91,92],90-[29,31,44,55,63,64,67,82,84,89,91],91-[33,40,42,44,48,49,57,63,65,67,69,70,71,72,75,83,84,89],92-[32,42,49,50,56,57,67,77,80,82,88,89],93-[47,51,55,57,58,70,73,75,79,82,88,90],94-[31,37,41,43,45,48,57,59,60,61,62,69,73,77,78,83,85,91,93],95-[32,39,42,43,47,49,53,61,64,68,77,81,83,84,88,90],96-[32,37,39,41,42,43,47,51,56,57,59,60,61,62,65,68,71,72,73,76,80,90],97-[45,46,51,55,60,61,63,64,73,75,77,84,91,93],98-[39,45,47,55,56,59,66,73,76,80,85],99-[31,32,36,38,39,45,48,51,52,53,67,68,71,77,79,84],100-[33,38,39,41,42,43,45,47,49,50,53,55,58,66,68,72,76,77,79,81,84,92,93],101-[32,33,43,49,53,57,58,59,60,69,72,81,82,85,89],102-[28,30,36,38,53,56,58,63,67,69,75,78,92,93],103-[31,35,38,40,41,50,52,56,60,62,69,74,79,84],104-[31,32,34,35,38,40,41,46,49,50,56,59,72,75,80,81,82,91,92],105-[30,32,42,43,48,56,66,67,70,72,75,83,85,90],106-[31,35,36,43,53,56,57,90],107-[31,38,39,41,49,52,53,57,60,68,72,78,91],108-[35,45,48,49,50,51,53,57,59,60,61,65,69],109-[32,37,38,42,44,45,46,48,52,59,63,75,77,79,81,82,83,89,92],110-[29,31,36,37,40,51,52,55,61,63,67,69,73,80,83,84],111-[35,39,43,45,50,56,59,63,78,79,80,82,87],112-[33,37,39,43,45,48,59,61,65,67,80,88],113-[59,63,65,75,84,87],114-[35,38,47,63,66,68,70,73,75,83,91],115-[30,36,38,55,64,69,70,73,75,79,82,87,88,90],116-[33,39,48,57,63,65,69,70,73,80,82,92],117-[39,43,45,48,55,60,61,64,68,75,89,93],118-[40,55,60,67,72,73,75,87,89,93],119-[32,33,38,45,46,50,51,56,58,59,64,72,75,89,92],120-[32,37,47,59,69,75,81,83,91,92],121-[31,32,45,47,48,58,62,64,67,83,84,85,90],122-[47,48,53,90,92],123-[49,50,51,53,59,60,64,72,79,85,91],124-[38,49,50,56,60,61,64,70,75,79,81,83,88,89,91],125-[40,42,45,48,62,63,67,70,76,82,84],126-[39,45,47,67,80,84,89],127-[31,38,39,42,57,58,62,65,71,75,76,77,79,81,83,90,93],128-[33,49,56,58,59,65,71,75,76,81,82,84],129-[39,45,50,51,53,55,60,77,79,80,81,88,91],130-[28,29,37,42,43,58,59,60,67,68,77,82,84,88,89,92,93],131-[33,36,37,44,45,46,48,59,61,70,71,84],132-[30,33,42,48,53,55,56,60,69,71,77,82,83],133-[33,43,52,55,60,68,70,71,73,77,82,83,91,93],134-[35,52,53,55,59,62,67,68,70,71,77,78,80,82,88,90,91],135-[28,31,32,41,44,47,57,59,60,64,67,81,89,92],136-[35,36,38,39,40,47,48,51,53,56,57,60,67,70,71,79,80,81,82,92],137-[32,33,42,51,57,59,65,66,71,72,78,80,82,85],138-[33,38,43,61,65,67,72],139-[31,33,35,39,42,45,46,63,65,67,69,71,79,81,87,89,93],140-[35,39,43,53,58,59,65,76,77,84,85,89],141-[50,53,58,59,61,63,69,79,80,82,84],142-[37,39,45,53,57,58,60,67,69,76,79,80,83,84,87,92],143-[33,50,53,77,82,85,91],144-[31,35,39,40,45,51,56,61,66,68,71,75,83],145-[47,57,59,60,64,70,71,72,82,83,84,88,91],146-[37,39,40,41,45,47,51,56,60,61,66,68,82,91,93],147-[34,46,56,58,60,61,70,83,85,93],148-[30,37,39,43,53,65,70,72,75,89],149-[41,43,48,63,67,70,82,90,91,92],150-[29,32,43,48,51,59,65,75,77,81,82,93],151-[31,37,48,56,58,67,68,73],152-[30,42,50,62,71,72,82,83],153-[36,45,47,50,53,58,65,71,72,83],154-[37,43,60,72,75,84,91],155-[39,44,45,48,60,70,73,75,79,83,89,90],156-[26,29,42,45,51,52,53,55,58,63,64,65,70,76,80,83,87,89],157-[41,43,45,48,56,65,71,73,75,76,82,84],158-[31,36,42,43,49,51,53,57,65,67,68,76,79,84,91],159-[39,45,52,53,59,63,68,80,81,85],160-[39,41,42,46,50,51,68,72,75,76,81,82],161-[36,45,48,49,55,61,64,66,67,72,73,77,79,80],162-[29,32,33,38,39,44,49,51,61,64,68,69,73,82,84,90,91,92,93],163-[36,45,49,50,53,62,70,72,77,84,90,92],164-[43,47,50,61,62,66,71,72,83,88],165-[29,33,45,61,70,73,75,79,91,93],166-[35,38,39,40,42,45,46,49,52,53,62,67,70,72,79,81,88],167-[31,33,36,37,39,41,48,59,65,83],168-[31,35,41,43,48,51,53,60,67,70,75,77,79,80,82,85,92,93],169-[33,42,51,61,66,69,72,73,76,83,88,90,91],170-[33,45,46,56,60,64,65,67,81,93],171-[27,32,35,39,42,48,65,68,69,77,80,83],172-[41,48,50,52,56,57,61,64,70,72,90,92],173-[33,47,57,58,68,80,83,84,91],174-[32,39,47,58,61,73,77,79,80,81,83,85,89],175-[38,42,43,45,53,57,59,60,62,65,67,69,72,73,75,80,81,84,88],176-[31,36,38,40,47,48,49,57,62,64,68,70,73,79,83,91],177-[35,36,39,40,51,52,59,65,66,67,68,89],178-[35,37,39,56,58,66,67,68,70,71,76,77,87,88,91,93],179-[35,42,53,57,58,61,64,68,69,70,79,81,84,85,88],180-[39,40,43,58,65,69,70,73,83,91],181-[38,42,47,48,57,60,62,63,66,67,75,83,84],182-[36,43,45,51,71,80,81,84],183-[38,42,46,51,56,61,62,70,72,73,81,82],184-[31,32,42,47,48,53,60,66,67,76,79,80,93],185-[30,39,45,47,48,52,56,57,60,75,79,80,81,83,85,87,91],186-[32,38,41,43,45,46,53,55,56,58,60,62,68,72,79],187-[33,37,41,45,48,50,58,69,75,80,84,92],188-[31,33,35,41,42,46,48,56,57,66,73,76,79,81,84,85,88,89],189-[55,56,69,84,89,90,91,92,93],190-[33,35,39,51,53,56,57,60,64,77,79,82,83,90],191-[29,33,36,39,40,42,43,47,50,51,56,60,69,70,71,76,79],192-[30,31,32,35,36,38,39,42,47,49,53,58,64,84,88,92],193-[50,51,61,62,64,65,69,81,83,84,89,91],194-[33,41,43,47,56,64,65,68,72,80,81,82,84,88],195-[38,42,50,51,59,63,67,75,77,85,88,89,92,93],196-[43,46,48,57,62,64,80,81,83,84,85,89],197-[40,48,50,61,62,66,71,75,82,88,89,93],198-[32,33,38,51,57,62,65,67,71,82,85,90,92],199-[35,36,39,41,43,49,51,58,60,62,67,68,73,79,80],200-[35,38,41,48,57,61,63,75,85,88,91,93]]).
negFP([201-[32,50,60,65,68,70,71,73,83,89,91,92],202-[27,29,30,31,33,37,40,42,49,51,53,71,73,80,81,84,85],203-[37,38,40,51,61,73,75,80,82,88,89,90],204-[29,39,46,51,56,59,60,61,67,68,75,83,85,88,91],205-[32,33,35,36,39,41,43,46,49,51,53,59,62,69,70,73,83],206-[25,28,29,45,46,47,56,60,65,69,70,83,85],207-[29,31,38,45,50,51,56,61,67,73,75,76,77,78,82,83,89],208-[32,35,36,37,39,45,47,60,61,69,76,88,91,92],209-[22,36,37,39,40,42,49,50,51,55,81,85,91],210-[29,41,53,66,69,71,75,83,85,88,91],211-[33,39,43,50,57,58,59,63,65,68,69,76,82,83,85,89],212-[25,26,27,31,33,35,38,47,50,61,62,72,77,79,85,89,92],213-[32,39,47,50,58,59,85,88,89,90,93],214-[28,31,32,33,56,63,64,79,81,83,84,85,88],215-[29,30,36,37,43,46,49,55,57,60,68,70,71,75,89,90],216-[33,37,39,44,47,49,52,57,61,65,66,70,75,76],217-[28,32,39,42,48,50,51,61,66,69,71,80,83,91,92],218-[25,37,39,41,45,49,56,59,60,70,71,73,80,83,89,90,93],219-[33,43,47,49,55,59,60,61,62,65,73,78,82,83,84,90,91],220-[30,33,35,39,50,53,60,62,82,90,91,93],221-[25,27,31,33,40,41,49,50,51,58,64,69,71,72,82,84],222-[28,31,32,35,39,40,41,42,43,45,48,51,56,62,63,68,69,73,80,83,84,88,92],223-[27,29,32,40,42,43,50,51,56,62,73,81],224-[31,40,42,49,50,52,53,63,66,71,73,75,76,77,82,89,91,92],225-[44,47,50,64,66,67,71,79,85,88,91,92],226-[26,32,36,37,40,42,43,47,48,57,61],227-[29,33,45,49,55,58,60,61,63,64,65,67,68,70,81,88,89,91,93],228-[27,31,33,39,40,46,47,49,53,59,60,66,69,70,72,80,84,88,89],229-[21,22,23,26,27,29,31,33,39,40,49,50,55,60,63,68,69,75,77,82,85],230-[26,36,42,48,50,51,55,58,59,61,62,63,64,71,76,79,80,81,85,88,93],231-[30,37,43,45,47,48,51,52,56,62,66,67,71,72,73,75,82,92],232-[38,42,53,57,58,69,71,73,76,77,84,88],233-[30,47,50,51,56,62,66,71,73,75,80,81,92],234-[36,40,42,47,49,50,53,61,64,67,73,74,77,79,80,82,85,92,93],235-[23,25,27,29,33,47,50,51,52,53,58,60,65,70,72,73,75,77,82,83,89,91],236-[35,36,38,41,42,43,52,56,58,59,61,69,70,76,80,81,83,85,88],237-[35,39,47,48,49,50,51,53,55,58,61,63,70,81,84,90],238-[30,37,43,45,48,51,52,63,64,67,68,70,75,77,84,85,89,92],239-[33,51,61,70,75,76,80,92],240-[47,51,58,60,65,67,72,75,85,90],241-[33,38,42,47,48,49,51,52,69,75,76,79,84,90],242-[26,27,31,36,38,39,41,43,49,55,59,69,71,75,82],243-[26,29,30,31,32,37,47,49,61,69,75,78,87,88,90],244-[31,40,41,47,48,58,59,71,75,82,85,93],245-[42,43,44,56,63,70,71,72,76,77,80,85,88,90],246-[36,41,45,47,49,63,64,70,71,73,81,85,90,92,93],247-[59,64,65,67,72,73,76,79,92,93],248-[33,38,45,49,50,51,64,70,76,81,83,85,91],249-[36,41,46,47,55,62,66,67,73,74,76,77,82,84,91,93],250-[32,33,37,41,47,48,50,64,68,73,75,80,82],251-[27,30,32,35,36,37,38,50,57,60,63,71,76,82,83,85,89,91,93],252-[27,29,35,42,49,51,56,57,65,68,76,79,82,83,89],253-[27,28,31,32,37,38,40,42,47,48,53,58,65,73,77,83,84,85,92],254-[30,33,37,41,43,49,53,56,64,67,70,71,75,76,80,84,92],255-[37,40,42,48,49,57,58,63,65,72,73,75,82,83,84,88,89,90],256-[25,40,47,49,57,58,61,64,68,70,78,82,83,87,90,93],257-[35,38,46,49,50,53,55,59,67,71,78,80,90,93],258-[26,27,29,35,39,42,53,61,65,68,75,77,80,82,85,91,92],259-[32,33,43,45,49,50,56,58,59,65,71,83,85,88],260-[25,28,32,36,39,42,47,49,57,62,66,67,70,75,76,77,81,88],261-[33,41,47,59,62,63,65,66,73,75,77,88],262-[25,26,33,37,38,40,43,44,45,47,50,52,57,60,63,67,69,70,71,80,85,87,88,90,91],263-[28,31,35,40,47,51,58,59,60,63,75,81,82,88,89,91],264-[26,31,32,38,45,47,59,72,73,75,80,82,90,93],265-[30,36,37,39,47,49,56,61,63,67,70,77,79,82,85,89,90],266-[27,36,37,39,40,46,55,56,61,62,71,72,73,76,82,91,93],267-[26,40,42,48,49,51,61,65,67,79,80,81,82,83,85,92],268-[29,40,46,50,51,66,68,72,73,82,83,85],269-[35,38,43,45,47,49,51,53,58,59,60,62,66,68,69,70,75,76],270-[33,38,43,47,49,52,56,58,60,65,72,73,75,83,88,89,93],271-[30,31,32,38,42,50,51,64,71,73,76,82,89],272-[29,33,35,40,42,43,47,49,60,67,68,69,73,75,79,81,83,84,85,91,93],273-[33,35,37,39,41,42,43,50,57,58,64,70,73,77,79,80,87,89],274-[45,51,57,59,60,62,63,69,71,76,77,82,89,90],275-[51,52,53,59,67,69,71,73,76,85,91],276-[26,27,28,29,37,38,39,45,46,47,48,49,51,52,59,61,62,63,67,82],277-[26,31,38,50,51,56,68,70,72,83,85],278-[31,39,42,50,59,71,73,80,88,90,91],279-[33,35,38,39,42,49,51,52,53,57,59,70,71,72,79,83,87,88,93],280-[30,37,40,42,46,56,62,64,66,68,69,70,79,80,81,83,88,90,91,92],281-[32,38,39,42,43,48,49,51,57,63,66,76,77,81,82,91],282-[28,29,31,32,33,36,38,39,46,47,50,58,61,66,82,85],283-[38,39,41,48,58,61,63,64,65,70,73,77,79,83,84,93],284-[31,36,37,43,45,53,62,65,69,70,72,79,80,81,85,90,93],285-[29,31,33,36,38,40,44,50,51,53,57,64,68,69,71,72,73,81,83,90,93],286-[31,39,49,50,55,57,58,59,62,70,75,77,83,84,91,92],287-[29,41,42,50,64,68,82,85,91,92],288-[27,28,29,35,41,45,48,49,57,63,70,71,76,81,83,84,92],289-[25,29,33,39,42,45,47,50,51,52,62,66,71,73,82,87],290-[37,39,43,45,49,53,64,70,71,73,75,79,82,88,92],291-[31,35,37,40,47,49,50,51,60,62,67,70,71,73,80,91],292-[28,29,32,37,38,40,42,46,49,50,51,56,57,60,62,63,67,73,75,77,79,81,85,89,93],293-[31,32,33,36,38,39,43,46,50,58,59,61,63,67,69,73,75,82,83],294-[40,47,50,51,55,57,58,65,70,72,81,84,85,88,89],295-[26,33,36,38,47,49,50,55,56,67,73,75,82,88,90],296-[27,29,32,45,47,50,51,57,60,61,62,65,81,84,85],297-[33,36,37,39,40,43,44,47,49,51,53,64,65,73,76,81,89],298-[42,57,59,61,63,68,69,71,75,82,89,91],299-[32,37,38,42,43,45,47,53,73,75,91],300-[40,42,49,61,62,70,71,75,76,82,88,90],301-[31,35,42,50,53,57,64,70,71,73,83,84,85],302-[33,35,39,41,51,56,57,59,64,65,71,72,80,81,85,90],303-[33,36,38,39,48,53,60,65,70,71,73,75,91,93],304-[31,38,40,45,56,61,64,71,77,81],305-[38,41,45,49,50,51,59,67,82,83,87],306-[31,32,35,36,38,40,42,61,70,71,72,73,76,78,80,84,90,91,92],307-[30,41,42,45,48,49,59,60,62,71,73,93],308-[27,30,35,41,51,56,59,61,63,67,72,73,79,92],309-[33,35,36,37,40,49,51,57,62,65,66,67,68,70,71,73,77,79,80,83,84,89],310-[41,42,47,75,77,79,81,85,90],311-[21,27,29,35,36,37,38,48,51,56,65,70,73,80,90,92],312-[35,37,42,44,46,49,51,53,55,59,68,79,85,89],313-[29,30,36,37,40,47,50,56,65,67,75,76,84,85,88,92,93],314-[32,35,38,44,58,60,61,63,69,73,90],315-[31,33,37,47,55,57,58,60,61,68,70,80,82,91],316-[31,42,50,51,58,71,72,73,80,81,87,89],317-[32,36,39,41,42,43,48,49,50,59,64,66,73,76,81,83],318-[35,40,49,58,72,75,79,83,84,89,91,92,93],319-[35,37,41,47,52,55,56,57,62,64,65,69,70,71,73,76,83,84,85,92],320-[35,38,40,51,57,62,68,70,71,78,79,81,85,91,92],321-[30,35,36,37,39,41,53,70,71,73,77,80],322-[25,31,35,36,47,49,50,59,61,63,66,68,71,80,81,83,85],323-[31,35,36,47,49,51,55,56,60,65,70,72,76,77,79,84,87,88],324-[28,29,35,39,41,49,51,53,56,57,59,64,66,75,76,83,89,92],325-[29,35,37,39,40,50,57,63,70,75,80,81,83,85,88],326-[30,32,33,35,36,37,42,49,60,63,68,70,81,89],327-[29,30,35,36,37,40,43,45,50,51,53,67,71,73,81,82,83,92,93],328-[33,41,51,53,56,57,65,69,71,76,79,84,85,88,92],329-[29,33,37,40,42,47,49,53,55,61,67,68,76,82],330-[29,31,32,38,39,43,51,52,56,57,63,68,71,72,75,79,82,85,88],331-[35,38,45,50,53,57,58,61,68,70,77,82,83,85,90],332-[35,37,40,43,53,56,59,62,71,73,75,77,81,88,89],333-[37,43,45,49,56,71,79,82,91,92],334-[25,45,49,50,56,60,68,75,82,85],335-[29,35,47,49,55,59,60,61,63,64,67,79,81,89,90],336-[30,33,36,41,43,47,55,56,61,73,75,79,81,82,84,85,89,90],337-[22,32,40,43,48,59,67,70,71,73,79,90],338-[29,35,36,40,49,50,51,55,61,62,70,80,82],339-[29,37,47,50,52,53,61,62,68,70,76,80,81,83,85,87,90],340-[25,26,30,31,33,38,40,52,63,73,82,84,90,91],341-[42,47,50,51,53,65,66,72,78,79,82,85,89],342-[25,31,43,49,55,57,66,70,77,80,88,91,92,93],343-[33,37,38,39,42,47,49,65,76,79,81,88,90],344-[29,31,32,38,43,51,55,56,57,58,59,60,64,68,71,73,79,82,83,85],345-[34,40,41,46,49,50,55,66,67,68,71,73,75,77,82],346-[30,32,35,38,43,47,49,50,53,59,60,63,73,75,79,81,82],347-[27,31,45,46,51,52,59,61,64,67,70,73,85,89],348-[29,47,48,49,50,61,67,72,76,79,87,93],349-[28,32,33,38,39,41,42,47,48,56,57,65,70,71,72,73,75,80,82,93],350-[37,45,50,58,63,64,66,71,75,76,82,85,92,93],351-[32,38,43,47,52,58,60,63,69,73,82,85],352-[31,42,47,52,57,61,64,73,75,90],353-[30,32,35,36,45,53,57,60,63,71,73,75,77,79,82,83,85,88],354-[34,36,42,45,46,50,52,55,56,58,59,62,66,70,73,82,83,84,89,92,93],355-[33,35,36,41,48,53,56,60,63,65,67,70,71,76,83,85],356-[33,36,43,47,49,56,57,63,67,71,75,77,84,88,92],357-[29,36,40,49,50,63,68,69,71,73,75,80],358-[27,37,42,46,47,50,52,57,58,60,62,64,73,75,79,80,82,85,92],359-[32,33,38,43,45,48,49,50,52,57,58,62,63,67,70,71,73,89,90,92],360-[32,36,38,41,44,51,67,70,71,72,73,74,80,82,84,90],361-[31,36,44,45,47,49,50,51,52,53,56,57,58,63,64,66,70,72,73,83,84],362-[29,33,36,41,43,46,48,66,73,81,82,83,87,90,91],363-[31,36,37,38,42,43,46,47,62,68,73,75,79,81,82,85,89],364-[39,43,47,59,60,63,70,73,75,77,81,84,89,90,92],365-[31,45,47,51,57,63,65,68,74,76,83,85,90],366-[26,27,28,30,34,36,40,48,49,50,51,54,59,60,63,64,65,70,72,77,78,79,81,90,92],367-[30,31,43,47,48,53,56,73,75,81,83,84,89,90],368-[44,58,60,63,66,73,75,88,91,93],369-[28,29,33,37,42,50,52,55,60,71,77,82,83,85,93],370-[29,32,38,42,47,49,57,65,79,82,83,89,90,93],371-[28,30,31,47,53,61,63,65,68,70,75,76,77,82,85,90],372-[38,42,43,48,49,50,51,53,61,63,70,72,81,82,83,91],373-[25,26,29,33,34,41,47,48,50,57,59,60,62,65,70,75,76,77,82,85,91,92],374-[27,30,32,34,35,40,44,49,50,51,56,57,60,75,77,90],375-[28,48,49,51,57,62,70,71,72,77,81,84],376-[30,33,35,40,51,58,60,62,69,71,72,73,78,80,84],377-[31,33,37,50,53,56,58,60,65,69,70,73,74,75,79,84,91,93],378-[29,46,47,58,65,70,83,85,90,92,93],379-[32,42,50,55,65,67,69,70,73,75,84,88,90,91,93],380-[27,52,61,62,65,67,68,70,77,78,83,92],381-[31,35,38,39,41,43,50,51,61,62,65,68,75,77,85,90],382-[27,31,44,49,50,55,58,59,67,71,73,76,78,91],383-[29,33,42,49,53,55,67,68,72,75,77,78,82,83,84],384-[23,27,35,38,52,53,61,67,68,69,70,76,77,81,82,89],385-[33,35,40,41,42,47,50,51,55,56,64,66,70,79,81,82,83,85,92,93],386-[30,41,48,58,69,70,75,77,79,80,82,85,89,93],387-[26,30,32,35,37,38,39,45,49,50,55,56,60,62,64,65,67,70,75,83,91,92],388-[38,42,51,60,64,71,77,79,85,89,92],389-[37,38,44,47,48,56,65,69,71,73,76,79,80,81,82,90],390-[28,30,32,35,39,50,61,65,69,70,73,76,80,83,85],391-[36,39,41,45,50,51,60,63,70,73,81,83,84,89,93],392-[33,37,41,45,49,50,65,66,75,80,83,88,89,91],393-[36,38,43,53,55,61,64,67,69,70,73,75,83,88,91],394-[29,30,36,38,43,48,49,50,53,55,57,61,64,68,77,80,82,83,89,93],395-[27,31,36,37,41,47,50,57,62,65,75,82],396-[36,39,47,51,59,60,64,66,67,69,73,75,76,80,81,83,88,90,93],397-[23,25,26,41,52,59,63,65,67,69,70,71,85,90],398-[31,32,33,36,42,45,52,56,59,61,62,64,71,73,77,79,80,82,85,88],399-[34,47,48,49,56,67,69,75,79,82,90],400-[37,43,47,49,50,51,53,56,65,71,76,81,82,83]]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% perfect_armg(+Clause, +ClauseSignature, +PosEIDs, +NegEIDs,
%              -PerfectARMG, -PerfectARMGSig, -PosEIDsCov, -NegEIDsCov)
%
% Given:
%   Clause: a list of literals representing a clause
%   ClauseSignature: list of signatures for Clause
%   PosEIDs: ordered list of positive example ids to consider to compute perfect armg
%   NegEIDs: ordered list of negative example ids to consider to compute perfect armg
%
% Returns:
%   PerfectARMG: a list of literals representing the best possible ARMG
%   PerfectARMGSig: PerfectARMG signature
%   PosEIDsCov: PerfectARMG positive coverage (subset of PosEIDs)
%   NegEIDsCov: PerfectARMG negative coverage (subset of NegEIDs)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

perfect_armg(Clause, ClauseSig, PosEIDs, NegEIDs,
             PerfectARMG, PerfectARMGSig, FPosEIDsCov, FNegEIDsCov):-
  posFP(PosFailProfile),
  negFP(NegFailProfile),
/*
  format("Initial clause:~n",[]), portray_clause(Clause),nl,
  format("Computing full positive fail profile~n",[]),
  examplesFullFailingProfile(Clause, ClauseSig, PosEIDs, PosFailProfile),
  write(PosFailProfile),nl,
  format("Computing full negative fail profile~n",[]),
  examplesFullFailingProfile(Clause, ClauseSig, NegEIDs, NegFailProfile),
  write(NegFailProfile),nl,
*/
  clean_fail_profile(PosFailProfile, [], CurPosFailProfile, CurPosEIDsCov),
  clean_fail_profile(NegFailProfile, [], CurNegFailProfile, CurNegEIDsCov),
  hypothesis_info(CurPosEIDsCov, CurNegEIDsCov, PosEIDs, NegEIDs, ClauseInfo),
  length(Clause, NumLiterals),
  format("PosCov:~w~n", [CurPosEIDsCov]),
  format("NegCov:~w~n", [CurNegEIDsCov]),
  format("about to loop~n",[]),
  perfect_armg_loop([], CurPosFailProfile, CurNegFailProfile, CurPosEIDsCov, CurNegEIDsCov, NumLiterals, ClauseInfo,
                    PosEIDsCov, NegEIDsCov, [], ClauseIndexsToRemove),
  format("loop ended~n",[]),
  remove_indexs_from_clause(Clause, ClauseSig, ClauseIndexsToRemove, TClause, TClauseSig),
  length(PosEIDsCov, NumPos1),
  length(NegEIDsCov, NumNegs1),
  format("Before reduction: NumPos:~w NumNeg:~w~n", [NumPos1, NumNegs1]),
  portray_clause(TClause),nl,
  negative_clause_reduce(TClause, TClauseSig, PosEIDs, NegEIDs, PosEIDsCov, NegEIDsCov,
                         PerfectARMG, PerfectARMGSig, FPosEIDsCov, FNegEIDsCov),
  length(FPosEIDsCov, NumPos2),
  length(FNegEIDsCov, NumNegs2),
  format("After reduction: NumPos:~w NumNeg:~w~n", [NumPos2, NumNegs2]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% remove_indexs_from_clause(+Clause, +ClauseSig, +ClauseIndexsToRemove, -NClause, -NClauseSig)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

remove_indexs_from_clause(Clause, ClauseSig, ClauseIndexsToRemove, NClause, NClauseSig):-
  remove_indexs_from_clause_aux(ClauseIndexsToRemove, 1, Clause, ClauseSig, NClause, NClauseSig).

remove_indexs_from_clause_aux([], _, C, S, C, S).
remove_indexs_from_clause_aux([CurIndex|Indexs], CurIndex, [_Lit|Lits], [_LSig|LSigs], NClause, NClauseSig):-
  !, NCurIndex is CurIndex+1,
  remove_indexs_from_clause_aux(Indexs, NCurIndex, Lits, LSigs, NClause, NClauseSig).
remove_indexs_from_clause_aux(Indexs, CurIndex, [Lit|Lits], [LSig|LSigs], [Lit|NLits], [LSig|NLitsSig]):-
  %the first index in Indes is greater than CurIndex
  NCurIndex is CurIndex+1,
  remove_indexs_from_clause_aux(Indexs, NCurIndex, Lits, LSigs, NLits, NLitsSig).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% clean_fail_profile(+FailProfile, +CurCoverage, -FinalFailProfile, -FinalCoverage)
%
% Given:
%  FailProfile: a term as described in examplesFullFailingProfile/4
%  CurCoverage: list of example ids covered 
%
% Returns:
%  FinalFailProfile: FailProfile with empty profiles removed
%  FinalCoverage: ids of the profiles removed (if the profile is empty that means the example is already covered)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

clean_fail_profile([], RCovIDs, [], CovIDs):-
  reverse(RCovIDs, CovIDs). % CurCoverage comes reversed
clean_fail_profile([EID-[]|T], CurCoverage, FinalFailProfile, FinalCoverage):-
  !,
  clean_fail_profile(T, [EID|CurCoverage], FinalFailProfile, FinalCoverage).
clean_fail_profile([H|T], CurCoverage, [H|R], FinalCoverage):-
  clean_fail_profile(T, CurCoverage, R, FinalCoverage).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% perfect_armg_loop(+GenPEIDs, +PosFailProfile, +NegFailProfile, +CurPosEIDsCov,
%                   +CurNegEIDsCov, +CurNumLiterals, +CurScoreInfo,
%                   -PosEIDsCov, -NegEIDsCov, +CurClauseIndexsRemoved, -FinalClauseIndexsRemoved)
%
% Gen
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

perfect_armg_loop(GenPEIDs, PosFailProfile, NegFailProfile, CurPosEIDsCov, CurNegEIDsCov, CurNumLiterals, CurScoreInfo,
                  FPosEIDsCov, FNegEIDsCov, CurCIndexsRemoved, FCIndexsRemoved):-
  (choose_best_indexs_to_remove(PosFailProfile, NegFailProfile, CurNumLiterals, CurScoreInfo,
                                (NPosFP, NNegFP, Score, EID-TIx2Rem, TPosEIDsCov, TNegEIDsCov)) ->
      ord_union(CurPosEIDsCov, TPosEIDsCov, NCurPosEIDsCov), % notice that TurnPosEIDsCov and CurPosEIDsCov do not intersect
      ord_union(CurNegEIDsCov, TNegEIDsCov, NCurNegEIDsCov), % idem for negatives
      ord_union(CurCIndexsRemoved, TIx2Rem, NCurCIndexsRemoved),
      ord_insert(GenPEIDs, EID, NGenPEIDs),
      update_score_info(CurScoreInfo, TPosEIDsCov, TNegEIDsCov, NScoreInfo),
      length(TIx2Rem, NumLitsRemoved),
      NNumLiterals is CurNumLiterals - NumLitsRemoved,
      length(NGenPEIDs, CurIter),
      length(DummyClause, NNumLiterals),
      format("IndexsToRemove:~w~n", [NCurCIndexsRemoved]),
      message(best_rmg, [CurIter, Score, DummyClause, NGenPEIDs, NCurPosEIDsCov, NCurNegEIDsCov]),
      perfect_armg_loop(NGenPEIDs, NPosFP, NNegFP, NCurPosEIDsCov, NCurNegEIDsCov, NNumLiterals, NScoreInfo,
                        FPosEIDsCov, FNegEIDsCov, NCurCIndexsRemoved, FCIndexsRemoved)
    ;
      format("no choice~n",[]),
      %no best choice, negatively reduce now
      FPosEIDsCov=CurPosEIDsCov,
      FNegEIDsCov=CurNegEIDsCov,
      FCIndexsRemoved=CurCIndexsRemoved
  ).

% update_score_info(+ScoreInfo, +PosEIDsCov, +NegEIDsCov, -NScoreInfo)

update_score_info([TP, FP, FN, TN], PosEIDsCov, NegEIDsCov, [NTP, NFP, NFN, NTN]):-
  exampleIDsWeights(PosEIDsCov, NewCovPosWeights),
  exampleIDsWeights(NegEIDsCov, NewCovNegWeights),
  ANewCovNegWeights is abs(NewCovNegWeights), %don't forget exampleIDs are not in absolute value
  NTP is TP + NewCovPosWeights,%    TP: True Positive weight
  NFP is FP + ANewCovNegWeights,%    FP: False Positive weight
  NFN is FN - NewCovPosWeights,%    FN: False Negative weight
  NTN is TN - ANewCovNegWeights.%    TN: True Negative weight

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% choose_best_indexs_to_remove(+PosFailProfile, +NegFailProfile, +NumLiterals, +ScoreInfo,
%                              -Result)
%
% Given:
%   PosFailProfile: current positive failing profile
%   NegFailProfile: current negative failing profile
%   NumLiterals: number of literals of the current implicit clause
%   ScoreInfo: [TP, FP, FN, TN] on the current implicit clause
%
% Returns:
%   Result: a term (NPosFailProfile, NNegFailProfile, Score, EID-IndexsToRemove, NPosEIDsCov, NNegEIDsCov)
%           where:
%             NPosFailProfile: PosFailProfile with PosEIDsCov removed
%             NNegFailProfile: NegFailProfile with NegEIDCov removed
%             Score: a number, the score of the clause after removing IndexsToRemove
%             EID: example ids choosed to removed this turn
%             IndexsToRemove: list of failing literals for EID with respect to the implicit clause so far
%             PosEIDsCov: ordered list of positive examples covered because of this choice of positive
%             NegEIDsCov: ordered list of negative examples covered because of this choice of negatives
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

choose_best_indexs_to_remove(PosFailProfile, NegFailProfile, NumLiterals, ScoreInfo, Result):-
  highest_scoring_example_for_armg(PosFailProfile, PosFailProfile, NegFailProfile, NumLiterals, ScoreInfo,
                                   Result).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% highest_scoring_example_for_armg(+CurFailProfile, +PosFailProfile, +NegFailProfile,
%                                  +NumLits, +ScoreInfo,
%                                  -(BestPosFailProfile, BestNegFailProfile,
%                                    BestScore, (BestID-BestIndexsToRemove),
%                                    BestPosEIDsCov, BestNegEIDsCov))
%
% Succeeds only if there is an improvement over base score
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

highest_scoring_example_for_armg(CurFailProfile, PosFailProfile, NegFailProfile, NumLits, ScoreInfo,
                                 BestScoreDS):-
  score(NumLits, ScoreInfo, MinScore), %MinScore is the score of the implicit clause
  InitScoreDS=(_, _, MinScore, _, _, _),
  highest_scoring_example_for_armg_aux(CurFailProfile, PosFailProfile, NegFailProfile, NumLits, ScoreInfo,
                                       InitScoreDS, BestScoreDS),
  BestScoreDS=(_, _, FinalScore, _, _, _),
  FinalScore>MinScore.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% highest_scoring_example_for_armg_aux(+CurFailProfile, +PosFailProfile, +NegFailProfile,
%                                      +NumLits, +ScoreInfo,
%                                      +(CurBestPosFailProfile, CurBestNegFailProfile,
%                                        CurBestScore, (CurID-CurBestIndexsToRemove),
%                                        CurBestPosEIDsCov, CurBestNegEIDsCov),
%                                      -(BestPosFailProfile, BestNegFailProfile,
%                                        BestScore, (BestID-BestIndexsToRemove),
%                                        BestPosEIDsCov, BestNegEIDsCov))
%
% Given:
%   NumLits: number of literals of current best clause (from previous iteration)
%   ScoreInfo: score info from the best clause (from previous iteration)
%
% Notes:
%   Only succeeds if a clause with score higher than inital score was found
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

highest_scoring_example_for_armg_aux([], _, _, _, _, Best, Best).
highest_scoring_example_for_armg_aux([(EID-IndexsToRemove)|T], PosFP, NegFP, NumLits, ScoreInfo, CurBest, FBest):-
  CurBest=(_, _, CurBestScore, _, _, _),
  score_for_armg_with_indexs_to_remove(IndexsToRemove, PosFP, NegFP, NumLits, ScoreInfo, CPosFP, CNegFP,
                                       CPosEIDsCov, CNegEIDsCov, CurScore, FNumLits, NScoreInfo),
  (verifies_partial_metrics(FNumLits, NScoreInfo), CurScore>CurBestScore -> % IndexsRem is the best indexs to remove
    format("New best score found:~w (example:~w)~n", [CurScore, EID]),
    NCurBest=(CPosFP, CNegFP, CurScore, (EID-IndexsToRemove), CPosEIDsCov, CNegEIDsCov),

    highest_scoring_example_for_armg_aux(T, PosFP, NegFP, NumLits, ScoreInfo, NCurBest, FBest)
   ;
  %the existing one is still the best
    highest_scoring_example_for_armg_aux(T, PosFP, NegFP, NumLits, ScoreInfo, CurBest, FBest)
  ).

%score_for_armg_with_indexs_to_remove(+IndexsToRemove, +PosFailProfile, +NegFailProfile,
%                                     +NumLiterals, +CurScoreInfo,
%                                     -NPosFailProfile, -NNegFailProfile,
%                                     -PosEIDsCov, -NegEIDsCov,
%                                     -Score, -FNumLits, -NScoreInfo)
score_for_armg_with_indexs_to_remove(IndexsToRemove, PosFailProfile, NegFailProfile,
                                     NumLits, CurScoreInfo, NPosFailProfile, NNegFailProfile,
                                     PosEIDsCov, NegEIDsCov, Score, FNumLits, NScoreInfo):-
  contains_indexs(PosFailProfile, IndexsToRemove, NPosFailProfile, PosEIDsCov),
  contains_indexs(NegFailProfile, IndexsToRemove, NNegFailProfile, NegEIDsCov),
  update_score_info(CurScoreInfo, PosEIDsCov, NegEIDsCov, NScoreInfo),
  length(IndexsToRemove, NumLitsToRemove),
  FNumLits is NumLits-NumLitsToRemove,
  score(FNumLits, NScoreInfo, Score).

% contains_indexs(+FailProfile, +Indexs, -NFailProfile, -EIDsContained)
contains_indexs([], _, [], []).
contains_indexs([(EID-FP)|T], Indexs, NFailProfile, [EID|EIDsC]):-
  ord_subset(FP, Indexs),!, % FP is contained in Indexs
  contains_indexs(T, Indexs, NFailProfile, EIDsC).
contains_indexs([(EID-FP)|T], Indexs, [(EID-NFP)|R], EIDsC):-
  ord_subtract(FP, Indexs, NFP), % update the failing profile with Indexs removed
  contains_indexs(T, Indexs, R, EIDsC).
